/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ β∧Applications of Circumscription to Formalizing Common Sense Knowledge

␈↓ α∧␈↓␈↓ αT(McCarthy␈α∂1980)␈α∞introduces␈α∂the␈α∞circumscription␈α∂method␈α∞of␈α∂non-monotonic␈α∂reasoning␈α∞and

␈↓ α∧␈↓gives␈αmotivation,␈αsome␈αmathematical␈αproperties␈αand␈αsome␈αexamples␈αof␈αits␈αapplication.␈α
 While␈αthe

␈↓ α∧␈↓present␈α⊃paper␈α⊃is␈α∩logically␈α⊃self-contained,␈α⊃motivation␈α⊃may␈α∩require␈α⊃some␈α⊃acquaintance␈α∩with␈α⊃the

␈↓ α∧␈↓earlier␈αpaper.␈α
 In␈αparticular␈α
we␈αdon't␈α
repeat␈αits␈α
arguments␈αabout␈α
the␈αimportance␈αof␈α
non-monotonic

␈↓ α∧␈↓reasoning in AI.  Also its examples are instructive.

␈↓ α∧␈↓␈↓ αTHere␈αwe␈αgive␈αa␈αmore␈αsymmetric␈α
definition␈αof␈αcircumscription␈αand␈αapplications␈αto␈αthe␈α
formal

␈↓ α∧␈↓expression␈α∂of␈α∂common␈α∂sense␈α∂facts.␈α∂ Our␈α∂goal␈α∂is␈α∂to␈α∂express␈α∂these␈α∂facts␈α∂in␈α∂a␈α∂way␈α∂that␈α∂would␈α∂be

␈↓ α∧␈↓suitable␈α∂for␈α⊂inclusion␈α∂in␈α∂a␈α⊂general␈α∂purpose␈α∂database␈α⊂of␈α∂common␈α∂sense␈α⊂facts.␈α∂ We␈α⊂imagine␈α∂this

␈↓ α∧␈↓database␈α
to␈α
be␈α
used␈α
by␈α
AI␈α
programs␈α
written␈α
after␈α
the␈α
initial␈α
preparation␈α
of␈α
the␈α
database.␈α
 It␈α
would

␈↓ α∧␈↓be␈α
best␈α
if␈α
the␈α
writers␈α∞of␈α
these␈α
programs␈α
didn't␈α
have␈α
to␈α∞be␈α
familiar␈α
with␈α
how␈α
the␈α∞common␈α
sense

␈↓ α∧␈↓facts␈α∃about␈α∀particular␈α∃phenomena␈α∃are␈α∀expressed.␈α∃ Thus␈α∃common␈α∀sense␈α∃knowledge␈α∃must␈α∀be

␈↓ α∧␈↓represented in a way that is not specific to a particular application.

␈↓ α∧␈↓␈↓ αTIt␈α∞turns␈α
out␈α∞that␈α
many␈α∞such␈α
common␈α∞sense␈α∞facts␈α
can␈α∞be␈α
formalized␈α∞in␈α
a␈α∞uniform␈α∞way.␈α
 A

␈↓ α∧␈↓single␈α∞predicate␈α∞␈↓↓ab,␈↓␈α∞standing␈α∞for␈α∞"abnormal"␈α∞is␈α∞circumscribed␈α∞with␈α∞certain␈α∞other␈α∞predicates␈α∞and

␈↓ α∧␈↓functions␈αconsidered␈αas␈α
variables␈αthat␈αcan␈α
be␈αconstrained␈αto␈α
achieve␈αthe␈αcircumscription␈αsubject␈α
to

␈↓ α∧␈↓the␈αaxioms.␈α So␈αfar␈α
this␈αseems␈αto␈αcover␈α
the␈αuse␈αof␈αcircumscription␈α
to␈αrepresesent␈αdefault␈αrules.␈α
 On

␈↓ α∧␈↓the␈αother␈αhand,␈αit␈αdoesn't␈αseem␈αthat␈αcircumscribing␈αabnormality␈αcan␈αbe␈αused␈αto␈αcover␈αmany␈αof␈αthe

␈↓ α∧␈↓examples␈αof␈α(McCarthy␈α1980)␈αin␈αwhich␈αwe␈αwant␈αto␈αlimit␈αa␈αset␈αto␈αthose␈αobjects␈αthat␈αcan␈αbe␈αshown

␈↓ α∧␈↓to be members.

␈↓ α∧␈↓␈↓ αTWe begin with our generalized circumscription.


␈↓ α∧␈↓␈↓αDefinition:␈↓␈α∞Let␈α∞␈↓↓A(P)␈↓␈α∞be␈α∞a␈α∞formula␈α∞of␈α∂second␈α∞order␈α∞logic␈α∞involving␈α∞a␈α∞tuple␈α∞␈↓↓P␈↓␈α∞of␈α∂free␈α∞predicate

␈↓ α∧␈↓symbols.␈α Let␈α␈↓↓E(P,x)␈↓␈αbe␈αa␈αwff␈αin␈αwhich␈α␈↓↓P␈↓␈αand␈αa␈αtuple␈α␈↓↓x␈↓␈αof␈αindividual␈αvariables␈αoccur␈αfree.␈α The

␈↓ α∧␈↓circumscription of ␈↓↓E(P,x)␈↓ relative to ␈↓↓A(P)␈↓ is the formula ␈↓↓A'(P)␈↓ defined by

␈↓ α∧␈↓1)␈↓ αt ␈↓↓A(P) ∧ ∀P'.[A(P') ∧ [∀x.E(P',x) ⊃ E(P,x)] ⊃ [∀x.E(P',x) ≡ E(P,x)]].␈↓
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓[We␈α∞are␈α∞here␈α∞writing␈α
␈↓↓A(P)␈↓␈α∞instead␈α∞of␈α∞␈↓↓A(P␈↓β1␈↓↓, . . . ,P␈↓βn␈↓↓)␈↓␈α
for␈α∞brevity␈α∞and␈α∞likewise␈α∞writing␈α
␈↓↓E(P,x)␈↓

␈↓ α∧␈↓instead␈α∩of␈α⊃␈↓↓E(P␈↓β1␈↓↓, . . . ,P␈↓βn␈↓↓,x␈↓β1␈↓↓, . . . ,x␈↓βn␈↓↓)␈↓.␈α∩ Likewise␈α⊃the␈α∩quantifier␈α⊃␈↓↓∀x␈↓␈α∩stands␈α∩for␈α⊃␈↓↓∀x␈↓β1␈↓↓ . . . x␈↓βn␈↓.

␈↓ α∧␈↓However, we don't use the full generality in this paper.


␈↓ α∧␈↓␈↓ αTThere␈α
are␈αtwo␈α
differences␈α
between␈αthis␈α
and␈α(McCarthy␈α
1980).␈α
 First,␈αin␈α
that␈α
paper␈α␈↓↓E(P,x)␈↓

␈↓ α∧␈↓had␈αthe␈αspecific␈αform␈α␈↓↓P(x).␈↓␈α
Here␈αwe␈αspeak␈αof␈αcircumscribing␈αa␈α
wff,␈αwhile␈αthere␈αwe␈αcould␈αspeak␈α
of

␈↓ α∧␈↓circumscribing␈α
a␈α
predicate.␈α
 We␈α
can␈α
still␈α
speak␈α
of␈α
circumscribing␈α
the␈α
predicate␈α
␈↓↓P␈↓␈α
when␈α
␈↓↓E(P,x)␈↓␈α
has

␈↓ α∧␈↓the␈α
special␈α
form␈α␈↓↓P(x).␈↓␈α
Second,␈α
in␈α(1)␈α
we␈α
use␈αan␈α
explicit␈α
quantifier␈αfor␈α
the␈α
predicate␈α
variable␈α␈↓↓P'␈↓

␈↓ α∧␈↓whereas␈αin␈α
(McCarthy␈α1980),␈α
the␈αformula␈α
was␈αa␈α
schema.␈α One␈α
advantage␈αof␈α
the␈αpresent␈α
formalism

␈↓ α∧␈↓is␈αthat␈αnow␈α␈↓↓A'(P)␈↓␈αis␈αthe␈αsame␈αkind␈αof␈αformula␈αas␈α␈↓↓A(P)␈↓␈αand␈αcan␈αbe␈αused␈αas␈αpart␈αof␈αthe␈αaxiom␈αfor

␈↓ α∧␈↓circumscribing some other wff.



␈↓ α∧␈↓1. A typology of uses of non-monotonic reasoning

␈↓ α∧␈↓␈↓ αTEach␈α∞of␈α∞the␈α∂several␈α∞papers␈α∞that␈α∂introduces␈α∞a␈α∞mode␈α∂of␈α∞non-monotonic␈α∞reasoning␈α∂seems␈α∞to

␈↓ α∧␈↓have␈αa␈αparticular␈αapplication␈αin␈αmind.␈α Perhaps␈αwe␈αare␈αlooking␈αat␈αdifferent␈αparts␈αof␈αan␈αelephant.

␈↓ α∧␈↓Therefore,␈α∞before␈α∞proceeding␈α∂to␈α∞applications␈α∞of␈α∂circumscription␈α∞I␈α∞want␈α∂to␈α∞suggest␈α∞a␈α∂typology␈α∞of

␈↓ α∧␈↓uses␈α
of␈α
non-monotonic␈α
reasoning.␈α
 The␈α
orientation␈αis␈α
towards␈α
circumscription,␈α
but␈α
I␈α
suppose␈αthe

␈↓ α∧␈↓considerations apply to other formalisms as well.

␈↓ α∧␈↓Non-monotonic reasoning has several uses.

␈↓ α∧␈↓1.␈αAs␈αa␈αcommunication␈αconvention.␈α Suppose␈αA␈αtells␈αB␈αabout␈αa␈αsituation␈αinvolving␈αa␈αbird.␈α If␈αthe

␈↓ α∧␈↓bird␈αcannot␈αfly,␈αand␈αthis␈αis␈αrelevant,␈αthen␈αA␈αmust␈αsay␈αso.␈α Whereas␈αif␈αthe␈αbird␈αcan␈αfly,␈αthere␈αis␈αno

␈↓ α∧␈↓requirement to mention the fact.

␈↓ α∧␈↓2.␈α⊂As␈α⊂a␈α⊃database␈α⊂or␈α⊂information␈α⊂storage␈α⊃convention.␈α⊂ It␈α⊂may␈α⊂be␈α⊃a␈α⊂convention␈α⊂of␈α⊃a␈α⊂particular

␈↓ α∧␈↓database␈αthat␈αcertain␈αpredicates␈αhave␈α
their␈αminimal␈αextension.␈α This␈αgeneralizes␈αthe␈α
closed␈αworld

␈↓ α∧␈↓assumption.␈α∀ When␈α∃a␈α∀database␈α∀makes␈α∃the␈α∀closed␈α∃world␈α∀assumption␈α∀for␈α∃all␈α∀predicates␈α∃it␈α∀is
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓reasonable␈α
to␈α
imbed␈α
this␈α
fact␈α
in␈α
the␈α
programs␈α
that␈α
use␈α
the␈α
database.␈α
 However,␈α
when␈α
there␈α
is␈α
a

␈↓ α∧␈↓priority␈α⊃structure␈α⊃among␈α⊃the␈α⊂predicates,␈α⊃we␈α⊃need␈α⊃to␈α⊃express␈α⊂the␈α⊃priorities␈α⊃as␈α⊃sentences␈α⊃of␈α⊂the

␈↓ α∧␈↓database,␈α
perhaps␈α
as␈α
a␈α
preamble␈α
to␈α
the␈αcollection␈α
of␈α
ground␈α
sentences␈α
that␈α
usually␈α
constitute␈αthe

␈↓ α∧␈↓main content.

␈↓ α∧␈↓␈↓ αTNeither␈α1␈α
nor␈α2␈αrequires␈α
that␈αmost␈αbirds␈α
can␈αfly.␈α Should␈α
it␈αhappen␈αthat␈α
most␈αbirds␈αthat␈α
are

␈↓ α∧␈↓subject␈αto␈αthe␈αcommunication␈αor␈αabout␈αwhich␈αinformation␈αis␈αrequested␈αfrom␈αthe␈αdata␈αbase␈αcannot

␈↓ α∧␈↓fly, the convention may lead to inefficiency but not incorrectness.

␈↓ α∧␈↓3.␈αAs␈α
a␈αrule␈α
of␈αconjecture.␈α
 This␈αuse␈αwas␈α
emphasized␈αin␈α
(McCarthy␈α1980).␈α
 The␈αcircumscriptions

␈↓ α∧␈↓may␈αbe␈αregarded␈αas␈αexpressions␈αof␈αsome␈αprobabilistic␈αnotions␈αsuch␈αas␈α"most␈αbirds␈αcan␈αfly"␈αor␈αthey

␈↓ α∧␈↓may␈α∞be␈α∞expressions␈α∂of␈α∞simple␈α∞cases.␈α∂ Thus␈α∞it␈α∞is␈α∂simple␈α∞to␈α∞conjecture␈α∂that␈α∞there␈α∞are␈α∂no␈α∞relevant

␈↓ α∧␈↓present␈α⊂material␈α⊂objects␈α⊂other␈α⊂than␈α∂those␈α⊂whose␈α⊂presence␈α⊂can␈α⊂be␈α∂inferred.␈α⊂ It␈α⊂is␈α⊂also␈α⊂a␈α∂simple

␈↓ α∧␈↓conjecture␈α
that␈α∞a␈α
tool␈α∞asserted␈α
to␈α
be␈α∞present␈α
is␈α∞usable␈α
for␈α
its␈α∞normal␈α
function.␈α∞ Such␈α
conjectures

␈↓ α∧␈↓sometimes␈α∂conflict,␈α⊂but␈α∂there␈α∂is␈α⊂nothing␈α∂wrong␈α∂with␈α⊂having␈α∂incompatible␈α∂conjectures␈α⊂on␈α∂hand.

␈↓ α∧␈↓Besides␈α
the␈αpossibility␈α
of␈αdeciding␈α
that␈αone␈α
is␈αcorrect␈α
and␈α
the␈αother␈α
wrong,␈αit␈α
is␈αpossible␈α
to␈αuse␈α
one

␈↓ α∧␈↓for generating possible exceptions to the other.

␈↓ α∧␈↓4.␈α
As␈α
a␈αrepresentation␈α
of␈α
a␈αpolicy.␈α
 The␈α
example␈αis␈α
Doyle's␈α
"The␈αmeeting␈α
will␈α
be␈α
on␈αWednesday

␈↓ α∧␈↓unless another decision is explicitly made".

␈↓ α∧␈↓5.␈α∂As␈α∂a␈α⊂very␈α∂streamlined␈α∂expression␈α∂of␈α⊂probabilistic␈α∂information␈α∂when␈α⊂numerical␈α∂probabilities,

␈↓ α∧␈↓especially␈α⊗conditional␈α∃probabilities,␈α⊗are␈α∃unobtainable.␈α⊗ Since␈α∃circumscription␈α⊗doesn't␈α∃provide

␈↓ α∧␈↓numerical␈α⊗probabilities,␈α⊗its␈α⊗probabilistic␈α↔interpetation␈α⊗involves␈α⊗probabilities␈α⊗that␈α↔are␈α⊗either

␈↓ α∧␈↓infinitesimal,␈αwithin␈αan␈αinfinitesimal␈αof␈αone,␈αor␈αintermediate␈α-␈αwithout␈αany␈αdiscrimination␈αamong

␈↓ α∧␈↓the␈αintermediate␈αvalues.␈α The␈αcircumscriptions␈αgive␈αconditional␈αprobabilities.␈α Thus␈αwe␈α
may␈αtreat

␈↓ α∧␈↓the␈α
probability␈αthat␈α
a␈αbird␈α
can't␈α
fly␈αas␈α
an␈αinfinitesimal.␈α
 However,␈α
if␈αthe␈α
rare␈αevent␈α
occurs␈αthat␈α
the

␈↓ α∧␈↓bird␈α
is␈αa␈α
penguin,␈α
then␈αthe␈α
conditional␈α
probability␈αthat␈α
it␈α
can␈αfly␈α
is␈α
infinitesimal,␈αbut␈α
we␈αmay␈α
hear

␈↓ α∧␈↓of some rare condition that would allow it to fly after all.
␈↓ α∧␈↓␈↓ u4


␈↓ α∧␈↓␈↓ αTWhy␈αdon't␈α
we␈αuse␈α
finite␈αprobabilities␈α
combined␈αby␈α
the␈αusual␈α
laws?␈α That␈α
would␈αbe␈α
fine␈αif

␈↓ α∧␈↓we␈α
had␈α
the␈α
numbers,␈α
but␈α
circumscription␈α
is␈α
usable␈αwhen␈α
we␈α
can't␈α
get␈α
the␈α
numbers␈α
or␈α
find␈αtheir

␈↓ α∧␈↓use␈αinconvenient.␈α Note␈α
that␈αthe␈αgeneral␈αprobability␈α
that␈αa␈αbird␈αcan␈α
fly␈αmay␈αbe␈αirrelevant,␈α
because

␈↓ α∧␈↓we␈α
are␈α
interested␈α
in␈α
the␈α
facts␈α
that␈α
influence␈αour␈α
opinion␈α
about␈α
whether␈α
a␈α
particular␈α
bird␈α
can␈αfly␈α
in

␈↓ α∧␈↓a particular situation.

␈↓ α∧␈↓␈↓ αTNotice␈αthat␈αcircumscription␈αdoes␈αnot␈αprovide␈αfor␈αweighing␈αevidence;␈αit␈αis␈αappropriate␈αwhen

␈↓ α∧␈↓the␈α∩information␈α∩permits␈α⊃snap␈α∩decisions.␈α∩ However,␈α⊃many␈α∩cases␈α∩nominally␈α⊃treated␈α∩in␈α∩terms␈α⊃of

␈↓ α∧␈↓weighing␈α∞information␈α∞are␈α∂in␈α∞fact␈α∞cases␈α∂in␈α∞which␈α∞the␈α∞weights␈α∂are␈α∞such␈α∞that␈α∂circumscription␈α∞and

␈↓ α∧␈↓other defaults work better.

␈↓ α∧␈↓6.␈αAuto-epistemic␈αreasoning.␈α "If␈αI␈α
had␈αan␈αelder␈αbrother,␈αI'd␈α
know␈αit".␈α This␈αhas␈αbeen␈α
studied␈αby

␈↓ α∧␈↓R. Moore.

␈↓ α∧␈↓7.␈αBoth␈αcommon␈α
sense␈αphysics␈αand␈α
common␈αsense␈αpsychology␈α
use␈αnon-monotonic␈αrules.␈α An␈α
object

␈↓ α∧␈↓will␈α
continue␈αin␈α
a␈αstraight␈α
line␈α
if␈αnothing␈α
interferes␈αwith␈α
it.␈α
 A␈αperson␈α
will␈αeat␈α
when␈αhungry␈α
unless

␈↓ α∧␈↓something␈α∪prevents␈α∩it.␈α∪ Such␈α∪rules␈α∩are␈α∪open␈α∩ended␈α∪about␈α∪what␈α∩might␈α∪prevent␈α∪the␈α∩expected

␈↓ α∧␈↓behavior,␈α
and␈α
this␈α∞is␈α
required,␈α
because␈α
we␈α∞are␈α
always␈α
encountering␈α
unexpected␈α∞phenomena␈α
that

␈↓ α∧␈↓modify␈α∂the␈α∂operation␈α∂of␈α∂our␈α∂rules.␈α∂ Science,␈α∂as␈α∂distinct␈α∂from␈α∂common␈α∂sense,␈α∂tries␈α∂to␈α∂work␈α∞with

␈↓ α∧␈↓exceptionless␈α⊂rules.␈α⊂ However,␈α⊂this␈α⊂means␈α⊂that␈α⊂common␈α⊂sense␈α⊂reasoning␈α⊂has␈α⊂to␈α⊂decide␈α⊃when␈α⊂a

␈↓ α∧␈↓scientific␈α
model␈α
is␈αapplicable,␈α
i.e.␈α
that␈α
there␈αare␈α
no␈α
important␈αphenomena␈α
not␈α
taken␈α
into␈αaccount

␈↓ α∧␈↓by the theories being used and the model of the particular phenomena.

␈↓ α∧␈↓␈↓ αTSeven␈α∩different␈α∩uses␈α∩for␈α∩non-monotonic␈α∪reasoning␈α∩seem␈α∩too␈α∩many,␈α∩so␈α∩perhaps␈α∪we␈α∩can

␈↓ α∧␈↓condense later.



␈↓ α∧␈↓2. Minimizing abnormality

␈↓ α∧␈↓␈↓ αTMany␈α⊂people␈α⊂have␈α⊂proposed␈α⊂representing␈α⊂facts␈α⊂about␈α⊂what␈α⊂is␈α⊂"normally"␈α⊂the␈α⊂case.␈α⊂ One
␈↓ α∧␈↓␈↓ u5


␈↓ α∧␈↓problem␈αis␈αthat␈αevery␈αobject␈αis␈αabnormal␈αin␈αsome␈αway,␈αand␈αwe␈αwant␈αto␈αallow␈αsome␈αaspects␈αof␈αthe

␈↓ α∧␈↓object␈αto␈αbe␈αabnormal␈αand␈αstill␈αassume␈αthe␈αnormality␈αof␈αthe␈αrest.␈α We␈αdo␈αthis␈αwith␈αa␈αpredicate␈α␈↓↓ab␈↓

␈↓ α∧␈↓standing␈α
for␈α
"abnormal".␈α We␈α
circumscribe␈α
␈↓↓ab z␈↓.␈α The␈α
argument␈α
of␈α␈↓↓ab␈↓␈α
will␈α
be␈αsome␈α
aspect␈α
of␈αthe

␈↓ α∧␈↓entities␈α
involved.␈α Some␈α
aspects␈α
can␈αbe␈α
abnormal␈α
without␈αaffecting␈α
others.␈α
 The␈αaspects␈α
themselves

␈↓ α∧␈↓are abstract entities, and their unintuitiveness is somewhat a blemish on the theory.

␈↓ α∧␈↓␈↓ αTHere are some applications.



␈↓ α∧␈↓3. Whether birds can fly

␈↓ α∧␈↓␈↓ αTMarvin␈α~Minsky␈α~(1982)␈α~offered␈α~expressing␈α~the␈α~facts␈α~and␈α~non-monotonic␈α→reasoning

␈↓ α∧␈↓concerning␈α⊂the␈α⊂ability␈α⊂of␈α⊂birds␈α⊂to␈α⊂fly␈α⊂as␈α∂a␈α⊂challenge␈α⊂to␈α⊂advocates␈α⊂of␈α⊂formal␈α⊂systems␈α⊂based␈α∂on

␈↓ α∧␈↓mathematical logic.

␈↓ α∧␈↓␈↓ αTThere␈α
are␈α
many␈α
ways␈α
of␈α
non-monotonically␈α
axiomatizing␈α
the␈α
facts␈α
about␈α
which␈α∞birds␈α
can

␈↓ α∧␈↓fly.  The following set of axioms using ␈↓↓ab␈↓ seems to me quite straightforward.

␈↓ α∧␈↓2)␈↓ αt ␈↓↓∀x.¬ab aspect1 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓Unless␈αan␈αobject␈αis␈αabnormal␈αin␈α␈↓↓aspect1,␈↓␈αit␈αcan't␈αfly.␈α (We're␈αusing␈αa␈αconvention␈αthat␈αparentheses

␈↓ α∧␈↓may␈α∪be␈α∀omitted␈α∪for␈α∪functions␈α∀and␈α∪predicates␈α∀of␈α∪one␈α∪argument,␈α∀so␈α∪that␈α∪(2)␈α∀is␈α∪the␈α∀same␈α∪as

␈↓ α∧␈↓␈↓↓∀x.(¬ab(aspect1(x) ⊃ ¬flies(x))␈↓.)

␈↓ α∧␈↓␈↓ αTNote␈α
that␈α
it␈α
wouldn't␈α
work␈α
to␈α
write␈α
␈↓↓ab␈α
x␈↓␈α
instead␈α
of␈α
␈↓↓ab␈α
aspect1␈α
x␈↓,␈α
because␈α
we␈α
don't␈α∞want␈α
a

␈↓ α∧␈↓bird␈α⊂that␈α⊂is␈α⊂abnormal␈α⊂with␈α⊂respect␈α⊂to␈α⊂its␈α⊂ability␈α⊂to␈α⊂fly␈α⊂to␈α⊂be␈α⊂automatically␈α⊂abnormal␈α⊂in␈α⊂other

␈↓ α∧␈↓respects.  Using aspects limits the effects of proofs of abnormality.

␈↓ α∧␈↓3)␈↓ αt ␈↓↓∀x.bird x ⊃ ab aspect1 x␈↓.

␈↓ α∧␈↓A␈αbird␈αis␈αabnormal␈αin␈α
␈↓↓aspect1,␈↓␈αso␈α(2)␈αcan't␈αbe␈α
used␈αto␈αshow␈αit␈αcan't␈α
fly.␈α If␈α(3)␈αwere␈αomitted,␈α
when

␈↓ α∧␈↓we␈α∩did␈α∩the␈α∩circumscription␈α∩we␈α⊃would␈α∩only␈α∩be␈α∩able␈α∩to␈α⊃infer␈α∩a␈α∩disjunction.␈α∩ Either␈α∩a␈α∩bird␈α⊃is

␈↓ α∧␈↓abnormal␈α∞in␈α
␈↓↓aspect1␈↓␈α∞or␈α
it␈α∞can␈α
fly␈α∞unless␈α
it␈α∞is␈α
abnormal␈α∞in␈α
␈↓↓aspect2.␈↓␈α∞(3)␈α
establishes␈α∞expresses␈α
our
␈↓ α∧␈↓␈↓ u6


␈↓ α∧␈↓preference␈α∂for␈α∞inferring␈α∂that␈α∞a␈α∂bird␈α∞is␈α∂abnormal␈α∞in␈α∂␈↓↓aspect1␈↓␈α∞rather␈α∂than␈α∞␈↓↓aspect2.␈↓␈α∂We␈α∞call␈α∂(3)␈α∞a

␈↓ α∧␈↓␈↓↓cancellation of inheritance␈↓ axiom.  We will see more of them.

␈↓ α∧␈↓4)␈↓ αt ␈↓↓∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x␈↓.

␈↓ α∧␈↓Unless a bird is abnormal in ␈↓↓aspect2,␈↓ it can fly.

␈↓ α∧␈↓5)␈↓ αt ␈↓↓∀x.ostrich x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓Ostriches␈α
are␈α
abnormal␈α
in␈α
␈↓↓aspect2.␈↓␈α
This␈α
doesn't␈α
say␈αthat␈α
an␈α
ostrich␈α
cannot␈α
fly␈α
-␈α
merely␈α
that␈α(4)

␈↓ α∧␈↓can't be used to infer that it does.  (5) is another cancellation of inheritance axiom.

␈↓ α∧␈↓6)␈↓ αt ␈↓↓∀x.penguin x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓Penguins are also abnormal in ␈↓↓aspect2.␈↓

␈↓ α∧␈↓7)␈↓ αt ␈↓↓∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓8)␈↓ αt ␈↓↓∀x.penguin x ∧¬ab aspect4 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓Normally␈α∞ostriches␈α∂and␈α∞penguins␈α∞can't␈α∂fly.␈α∞ However,␈α∞there␈α∂is␈α∞an␈α∞out.␈α∂ (7)␈α∞and␈α∞(8)␈α∂provide␈α∞that

␈↓ α∧␈↓under␈α⊃unspecified␈α⊃conditions,␈α⊃an␈α⊃ostrich␈α⊃or␈α⊃penguin␈α⊃might␈α⊃fly␈α⊃after␈α⊃all.␈α⊃ If␈α⊃we␈α⊃give␈α∩no␈α⊃such

␈↓ α∧␈↓conditions,␈αwe␈α
will␈αconclude␈α
that␈αan␈α
ostrich␈αor␈α
penguin␈αcan't␈α
fly.␈α Additional␈α
objects␈αthat␈α
can␈αfly

␈↓ α∧␈↓may␈α∂be␈α∂specified.␈α⊂ Each␈α∂needs␈α∂two␈α∂axioms.␈α⊂ The␈α∂first␈α∂says␈α∂that␈α⊂it␈α∂is␈α∂abnormal␈α∂in␈α⊂␈↓↓aspect1␈↓␈α∂and

␈↓ α∧␈↓prevents␈α(2)␈αfrom␈αbeing␈αused␈αto␈αsay␈αthat␈αit␈αcan't␈αfly.␈α The␈αsecond␈αprovides␈αthat␈αit␈αcan␈αfly␈αunless␈αit

␈↓ α∧␈↓is abnormal in yet another way.  Likewise additional non-flying birds can be provided for.

␈↓ α∧␈↓␈↓ αTWe␈α
haven't␈αyet␈α
said␈αthat␈α
ostriches␈αand␈α
penguins␈αare␈α
birds,␈αso␈α
let's␈αdo␈α
that␈αand␈α
throw␈αin␈α
that

␈↓ α∧␈↓canaries are birds also.

␈↓ α∧␈↓9)␈↓ αt ␈↓↓∀x.ostrich x ⊃ bird x␈↓

␈↓ α∧␈↓10)␈↓ αt ␈↓↓∀x.penguin x ⊃ bird x␈↓

␈↓ α∧␈↓11)␈↓ αt ␈↓↓∀x.canary x ∧ ¬ab aspect5 x ⊃ bird x␈↓.

␈↓ α∧␈↓We␈α∂threw␈α∂in␈α⊂␈↓↓aspect5␈↓␈α∂just␈α∂in␈α⊂case␈α∂one␈α∂wanted␈α⊂to␈α∂use␈α∂the␈α⊂term␈α∂canary␈α∂in␈α⊂the␈α∂sense␈α∂of␈α⊂a␈α∂1930s

␈↓ α∧␈↓gangster movie.
␈↓ α∧␈↓␈↓ u7


␈↓ α∧␈↓Asserting␈α
that␈α
ostriches,␈α
penguins␈α
and␈α
canaries␈α∞are␈α
birds␈α
will␈α
help␈α
inherit␈α
other␈α∞properties␈α
from

␈↓ α∧␈↓the class of birds.  For example, we have

␈↓ α∧␈↓12)␈↓ αt ␈↓↓∀x. bird x ∧ ¬ab aspect6 x ⊃ feathered x␈↓.

␈↓ α∧␈↓So␈αfar␈αthere␈α
is␈αnothing␈αto␈α
prevent␈αostriches,␈αpenguins␈αand␈α
canaries␈αfrom␈αoverlapping.␈α
 We␈αcould

␈↓ α∧␈↓write disjointness axioms like

␈↓ α∧␈↓13)␈↓ αt␈↓↓∀x. ¬ostrich x ∨ ¬penguin x␈↓,

␈↓ α∧␈↓but␈α
we␈α
would␈α
require␈α
␈↓↓n␈↓∧2␈↓␈α
of␈α
them␈α
if␈α
we␈α
have␈α
␈↓↓n␈↓␈α
species.␈α
 This␈α
problem␈α
is␈α
like␈α
the␈α
unique␈αnames

␈↓ α∧␈↓problem.


␈↓ α∧␈↓4. The unique names hypothesis

␈↓ α∧␈↓␈↓ αTRaymond␈α→Reiter␈α→(1979)␈α→introduced␈α→the␈α→phrase␈α→"unique␈α→names␈α→hypothesis"␈α~for␈α→the

␈↓ α∧␈↓assumption␈αthat␈α
distinct␈αnames␈αdenote␈α
distinct␈αobjects.␈α We␈α
want␈αto␈αtreat␈α
this␈αnon-monotonically.

␈↓ α∧␈↓Namely,␈α∩we␈α⊃would␈α∩like␈α∩to␈α⊃distinguish␈α∩those␈α∩models␈α⊃of␈α∩our␈α∩initial␈α⊃assumptions␈α∩in␈α∩which␈α⊃two

␈↓ α∧␈↓individual␈α⊗constants␈α⊗denote␈α⊗distinct␈α⊗objects␈α↔unless␈α⊗their␈α⊗equality␈α⊗is␈α⊗a␈α⊗consequence␈α↔of␈α⊗the

␈↓ α∧␈↓assumptions.␈α While␈α
we're␈αat␈α
it,␈αwe␈αmight␈α
as␈αwell␈α
try␈αfor␈αsomething␈α
stronger.␈α Two␈α
distinct␈αterms

␈↓ α∧␈↓should␈α⊂denote␈α⊂distinct␈α⊂objects␈α⊂unless␈α⊂their␈α⊂equality␈α⊂is␈α⊂a␈α⊂consequence.␈α⊂ This␈α⊂would␈α⊃include␈α⊂the

␈↓ α∧␈↓notion common in geometry of a figure being in general position.

␈↓ α∧␈↓␈↓ αTWe␈α∩don't␈α∩know␈α∩a␈α∩completely␈α∩satisfactory␈α∩way␈α⊃of␈α∩doing␈α∩this.␈α∩ Suppose␈α∩that␈α∩we␈α∩have␈α⊃a

␈↓ α∧␈↓language␈α∂␈↓↓L␈↓␈α∂and␈α∂a␈α∂theory␈α∂␈↓↓T␈↓␈α∂consisting␈α∂of␈α⊂the␈α∂consequences␈α∂of␈α∂a␈α∂formula␈α∂␈↓↓A.␈↓␈α∂It␈α∂would␈α⊂be␈α∂most

␈↓ α∧␈↓pleasant␈α
if␈α
we␈α
could␈α∞just␈α
circumscribe␈α
equality,␈α
but␈α
as␈α∞Ray␈α
Reiter␈α
(to␈α
be␈α
published)␈α∞has␈α
pointed

␈↓ α∧␈↓out,␈α∂this␈α∂doesn't␈α∂work,␈α∂and␈α∂nothing␈α∂similar␈α∂works.␈α∂ We␈α∂could␈α∂hope␈α∂to␈α∂circumscribe␈α∂some␈α∂other

␈↓ α∧␈↓formula␈α∞of␈α∞the␈α∂␈↓↓L,␈↓␈α∞but␈α∞this␈α∂doesn't␈α∞seem␈α∞to␈α∞work␈α∂either.␈α∞ Failing␈α∞that,␈α∂we␈α∞could␈α∞hope␈α∂for␈α∞some

␈↓ α∧␈↓other␈α
second␈α
order␈αformula␈α
taken␈α
from␈α
␈↓↓L␈↓␈αthat␈α
would␈α
express␈α
the␈αunique␈α
names␈α
hypothesis,␈αbut␈α
we

␈↓ α∧␈↓don't presently see how to do it.

␈↓ α∧␈↓␈↓ αTOur␈α⊃solution␈α∩involves␈α⊃extending␈α∩the␈α⊃language␈α∩by␈α⊃introducing␈α∩the␈α⊃names␈α∩themselves␈α⊃as

␈↓ α∧␈↓objects.  It also involves some other unpleasant conventions as we shall see.
␈↓ α∧␈↓␈↓ u8


␈↓ α∧␈↓␈↓ αTWe␈α
introduce␈α
names␈α
as␈α
objects␈α
and␈α
suppose␈α∞our␈α
theory␈α
is␈α
such␈α
that␈α
they␈α
are␈α∞all␈α
provably

␈↓ α∧␈↓distinct.␈α∂ There␈α∂are␈α⊂several␈α∂ways␈α∂of␈α∂doing␈α⊂this.␈α∂ Let␈α∂the␈α∂names␈α⊂be␈α∂␈↓↓n1,␈↓␈α∂␈↓↓n2,␈↓␈α∂etc.␈α⊂ The␈α∂simplest

␈↓ α∧␈↓solution␈αis␈αto␈αhave␈αan␈αaxiom␈α␈↓↓ni ≠nj␈↓␈αfor␈αeach␈αpair␈αof␈αdistinct␈αnames.␈α This␈αrequires␈αa␈α
number␈αof

␈↓ α∧␈↓axioms␈α∂proportional␈α∂to␈α∂the␈α∂square␈α∂of␈α⊂the␈α∂number␈α∂of␈α∂names,␈α∂which␈α∂is␈α⊂sometimes␈α∂objectionable.

␈↓ α∧␈↓The␈α∂next␈α∂solution␈α∂involves␈α∂introducing␈α∂an␈α∂arbitrary␈α∂ordering␈α∂on␈α∂the␈α∂names.␈α∂ We␈α⊂have␈α∂special

␈↓ α∧␈↓axioms␈α→␈↓↓n1 < n2,␈α→n2 < n3,␈α_n3 < n4␈↓,␈α→etc.␈α→and␈α_the␈α→general␈α→axioms␈α→␈↓↓∀x y.x < y ⊃ x ≠ y␈↓␈α_and

␈↓ α∧␈↓␈↓↓∀x y z. x < y ∧ y < z ⊃ x < z␈↓.␈α∞ This␈α∞makes␈α∞the␈α∞number␈α
of␈α∞axioms␈α∞proportional␈α∞to␈α∞the␈α∞number␈α
of

␈↓ α∧␈↓names.␈α↔ A␈α↔third␈α↔possibility␈α↔involves␈α↔mapping␈α↔the␈α↔names␈α↔onto␈α↔integers␈α↔with␈α↔axioms␈α↔like

␈↓ α∧␈↓␈↓↓index n1 = 1,␈α∪index n2 = 2␈↓,␈α∀etc.␈α∪and␈α∀using␈α∪a␈α∀theory␈α∪of␈α∀the␈α∪integers␈α∀that␈α∪provides␈α∀for␈α∪their

␈↓ α∧␈↓distinctness.␈α The␈αfourth␈αpossibility␈αinvolves␈αusing␈αstring␈αconstants␈αfor␈αthe␈αnames␈αand␈α"attaching"

␈↓ α∧␈↓to␈α∂equality␈α∂in␈α∂the␈α∂language␈α∂a␈α∂subroutine␈α⊂that␈α∂computes␈α∂whether␈α∂two␈α∂strings␈α∂are␈α∂equal.␈α⊂ If␈α∂our

␈↓ α∧␈↓names␈α∂were␈α∂quoted␈α∂symbols␈α⊂as␈α∂in␈α∂LISP,␈α∂this␈α∂amounts␈α⊂to␈α∂having␈α∂␈↓↓'a ≠ 'b␈↓␈α∂and␈α∂all␈α⊂its␈α∂countable

␈↓ α∧␈↓infinity of analogs as axioms.  Each of these devices is useful in appropriate circumstances.

␈↓ α∧␈↓␈↓ αTFrom␈α∞the␈α∞point␈α∞of␈α
view␈α∞of␈α∞mathematical␈α∞logic,␈α
there␈α∞is␈α∞no␈α∞harm␈α
in␈α∞having␈α∞an␈α∞infinity␈α
of

␈↓ α∧␈↓such␈α∞axioms.␈α∞ From␈α∞the␈α∂computational␈α∞point␈α∞of␈α∞view␈α∞of␈α∂a␈α∞theorem␈α∞proving␈α∞or␈α∂problem␈α∞solving

␈↓ α∧␈↓program,␈α
we␈α
merely␈α
suppose␈α
that␈αwe␈α
rely␈α
on␈α
the␈α
computer␈αto␈α
generate␈α
the␈α
assertion␈α
that␈αtwo␈α
names

␈↓ α∧␈↓are␈α
distinct␈α
whenever␈α
this␈α
is␈α
required,␈α
since␈α
a␈α
subroutine␈α
can␈α
easily␈α
tell␈α
whether␈α
two␈α
strings␈αare␈α
the

␈↓ α∧␈↓same.

␈↓ α∧␈↓␈↓ αT[One␈α
might␈α
suppose␈α
that␈α
some␈α
metamathematical␈α
considerations␈α
would␈α
change␈α∞from␈α
using

␈↓ α∧␈↓an␈α∩infinity␈α∩of␈α∩axioms,␈α⊃but␈α∩usually␈α∩this␈α∩won't␈α⊃be␈α∩so,␈α∩because␈α∩we␈α⊃can␈α∩generate␈α∩an␈α∩infinity␈α⊃of

␈↓ α∧␈↓provably␈α∞distinct␈α∞objects␈α∞from␈α∞a␈α
finite␈α∞set␈α∞of␈α∞axioms.␈α∞ All␈α∞we␈α
need␈α∞do␈α∞is␈α∞use␈α∞integers␈α∞as␈α
names,

␈↓ α∧␈↓axiomatize␈α
>␈αas␈α
a␈αrelation␈α
including␈α
its␈αtransitivity␈α
and␈αhave␈α
an␈αaxiom␈α
␈↓↓∀x y.x > y ⊃ x ≠ y␈↓.␈α
 It␈αis

␈↓ α∧␈↓equally␈α∩feasible␈α∩to␈α∩finitely␈α∩axiomatize␈α∩strings␈α∩in␈α⊃a␈α∩way␈α∩that␈α∩ensures␈α∩that␈α∩distinct␈α∩strings␈α⊃are

␈↓ α∧␈↓provably␈αdistinct.␈α The␈αaxiom␈αsystems␈αrequired␈αcan␈αbe␈αmuch␈αweaker␈αthan␈αPeano␈αarithmetic,␈αsince

␈↓ α∧␈↓induction is not required to prove particular instances of inequality.]
␈↓ α∧␈↓␈↓ u9


␈↓ α∧␈↓␈↓ αTWhenever␈αwe␈αdon't␈αcare␈αabout␈αthe␈αpossibility␈αof␈αsometimes␈αproving␈αthat␈αtwo␈αof␈αthe␈αobjects

␈↓ α∧␈↓denoted by a collection of names are equal, we can use axioms like

␈↓ α∧␈↓␈↓ αT14)␈↓ αt ␈↓↓name john = 'john ∧ name mike = 'mike␈↓

␈↓ α∧␈↓␈↓ αTand␈α∂this␈α∂gives␈α∂the␈α∂distinctness␈α∂of␈α∂the␈α∂objects␈α∂as␈α∂a␈α∂consequence␈α∂of␈α∂the␈α∂distinctness␈α∂of␈α∂the

␈↓ α∧␈↓names.

␈↓ α∧␈↓␈↓ αTHowever,␈α⊂this␈α⊃is␈α⊂too␈α⊃absolute␈α⊂for␈α⊃many␈α⊂applications.␈α⊃ It␈α⊂is␈α⊃often␈α⊂preferable␈α⊃that␈α⊂objects

␈↓ α∧␈↓denoted␈αby␈αdistinct␈αnames␈αare␈αto␈αbe␈αpresumed␈αdistinct␈αunless␈αthere␈αis␈αreason␈αto␈αbelieve␈αthem␈αto␈αbe

␈↓ α∧␈↓the␈αsame.␈α We␈αcan␈αdo␈αthis␈αas␈αfollows.␈α We␈αintroduce␈αa␈αpredicate␈α␈↓↓e(x,y)␈↓␈αand␈αaxiomatize␈αit␈αto␈αbe␈αan

␈↓ α∧␈↓equivalence␈αrelation.␈α Its␈αintended␈αinterpretation␈αis␈αthat␈αthe␈αnames␈α␈↓↓x␈↓␈αand␈α␈↓↓y␈↓␈αdenote␈αdistinct␈αobjects.

␈↓ α∧␈↓We␈αthen␈αformulate␈αall␈αour␈αusual␈αaxioms␈αin␈αterms␈αof␈αnames␈αrather␈αthan␈αin␈αterms␈αof␈αobjects.␈α Thus

␈↓ α∧␈↓␈↓↓on(n1,n2)␈↓␈α
means␈α
that␈α
the␈αobject␈α
named␈α
by␈α
␈↓↓n1␈↓␈αis␈α
on␈α
the␈α
object␈αnamed␈α
by␈α
␈↓↓n2,␈↓␈α
and␈α
␈↓↓bird x␈↓␈αmeans

␈↓ α∧␈↓that␈α⊂the␈α∂name␈α⊂␈↓↓x␈↓␈α⊂denotes␈α∂a␈α⊂bird.␈α⊂ We␈α∂add␈α⊂axioms␈α⊂of␈α∂substitutivity␈α⊂for␈α⊂␈↓↓e␈↓␈α∂with␈α⊂regard␈α⊂to␈α∂those

␈↓ α∧␈↓predicates␈α
that␈α
are␈α
translates␈αof␈α
predicates␈α
referring␈α
to␈α
objects␈αrather␈α
than␈α
predicates␈α
on␈αthe␈α
names

␈↓ α∧␈↓themselves.  Thus we have the axiom

␈↓ α∧␈↓␈↓ αT15)␈↓ αt ␈↓↓∀n1 n2 n1' n2'.e(n1,n1') ∧ e(n2,n2') ⊃ (on(n1,n2) ≡ on(n1',n2')␈↓.

␈↓ α∧␈↓␈↓ αTNow␈α⊃circumscribing␈α⊃␈↓↓e(x,y)␈↓␈α⊃gives␈α⊃the␈α⊃unique␈α⊃names␈α⊃hypothesis.␈α⊃ An␈α⊃example␈α⊃of␈α⊃such␈α⊃a

␈↓ α∧␈↓circumscription␈αis␈αgiven␈αin␈αAppendix␈αB.␈α However,␈αthere␈αis␈αa␈αprice.␈α The␈αcheap␈αpart␈αof␈αthe␈αprice

␈↓ α∧␈↓is␈α∪that␈α∀we␈α∪omit␈α∀substitutivity␈α∪axioms␈α∀for␈α∪predicates␈α∀and␈α∪functions␈α∀operating␈α∪on␈α∀the␈α∪names

␈↓ α∧␈↓themselves.␈α In␈αparticular,␈αwe␈α
don't␈αhave␈αan␈αaxiom␈αmaking␈α
equality␈αsubstitutive␈αwith␈αrespect␈αto␈α
␈↓↓e,␈↓

␈↓ α∧␈↓i.e. we don't have

␈↓ α∧␈↓␈↓ αT* ␈↓↓∀n1 n2 n1' n2'.e(n1,n1') ∧ e(n2,n2') ⊃ (n1 = n2) ≡ n1' = n2')␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α
expensive␈α
part␈α
of␈α
the␈α
price␈α
is␈α∞that␈α
we␈α
must␈α
refrain␈α
from␈α
any␈α
functions␈α∞whose␈α
values

␈↓ α∧␈↓are␈α⊃the␈α∩objects␈α⊃themselves␈α⊃rather␈α∩than␈α⊃names.␈α∩ They␈α⊃would␈α⊃spoil␈α∩the␈α⊃circumscription␈α∩by␈α⊃not

␈↓ α∧␈↓allowing us to infer the distinctness of the objects denoted by distinct names.


␈↓ α∧␈↓␈↓ αT5. Two examples of Raymond Reiter
␈↓ α∧␈↓␈↓ f10


␈↓ α∧␈↓␈↓ αTReiter␈α∃asks␈α∃about␈α∃representing,␈α∃"Quakers␈α∀are␈α∃normally␈α∃pacifists␈α∃and␈α∃Republicans␈α∀are

␈↓ α∧␈↓normally␈α
non-pacificists.␈α How␈α
about␈αNixon,␈α
who␈αis␈α
both␈αa␈α
Quaker␈αand␈α
a␈α
Republican?"␈αSystems

␈↓ α∧␈↓of␈αnon-monotonic␈α
reasoning␈αthat␈α
use␈αnon-provability␈α
as␈αa␈α
basis␈αfor␈α
inferring␈αnegation␈α
will␈αinfer

␈↓ α∧␈↓that␈αNixon␈α
is␈αneither␈α
a␈αpacifist␈α
nor␈αa␈α
non-pacifist.␈α Combining␈α
these␈αconclusions␈α
with␈αthe␈α
original

␈↓ α∧␈↓premiss leads to a contradiction.

␈↓ α∧␈↓␈↓ αTWe use

␈↓ α∧␈↓␈↓ αT16)␈↓ αt ␈↓↓∀x.quaker x ∧ ¬ab aspect1 x ⊃ pacifist x␈↓,

␈↓ α∧␈↓␈↓ αT17)␈↓ αt ␈↓↓∀x.republican x ∧ ¬ab aspect2 x ⊃ ¬ pacifist x␈↓

␈↓ α∧␈↓␈↓ αTand

␈↓ α∧␈↓␈↓ αT18)␈↓ αt ␈↓↓quaker Nixon ∧ republican Nixon␈↓.

␈↓ α∧␈↓␈↓ αTWhen␈α∞we␈α∞circumscribe␈α∂␈↓↓ab z␈↓␈α∞using␈α∞these␈α∞three␈α∂sentences␈α∞as␈α∞␈↓↓A(ab),␈↓␈α∞we␈α∂will␈α∞only␈α∞be␈α∂able␈α∞to

␈↓ α∧␈↓conclude␈αthat␈αNixon␈αis␈α
either␈αabnormal␈αin␈α␈↓↓aspect1␈↓␈α
or␈αin␈α␈↓↓aspect2,␈↓␈αand␈αwe␈α
will␈αnot␈αbe␈αable␈α
to␈αsay

␈↓ α∧␈↓whether he is a pacifist.

␈↓ α∧␈↓␈↓ αTReiter's␈αsecond␈αexample␈αis␈αthat␈αa␈αperson␈αnormally␈αlives␈αin␈αthe␈αsame␈αcity␈αas␈αhis␈αwife␈α
and␈αin

␈↓ α∧␈↓the␈αsame␈αcity␈αas␈αhis␈αemployer.␈α But␈αA's␈αwife␈αlives␈αin␈αVancouver␈αand␈αA's␈αemployer␈αis␈αin␈αToronto.

␈↓ α∧␈↓We write

␈↓ α∧␈↓␈↓ αT19)␈↓ αt ␈↓↓∀x.¬ab aspect1 x ⊃ city x = city wife x␈↓

␈↓ α∧␈↓␈↓ αTand

␈↓ α∧␈↓␈↓ αT20)␈↓ αt ␈↓↓∀x.¬ab aspect2 x ⊃ city x = city employer x␈↓.

␈↓ α∧␈↓␈↓ αTIf we have

␈↓ α∧␈↓␈↓ αT21)␈↓ αt ␈↓↓city wife A = Vancouver ∧ city employer A = Toronto ∧ Toronto ≠ Vancouver␈↓,

␈↓ α∧␈↓␈↓ αTwe␈α
will␈αagain␈α
only␈αbe␈α
able␈α
to␈αconclude␈α
that␈αA␈α
lives␈α
either␈αin␈α
Toronto␈αor␈α
Vancouver.␈α In␈α
this

␈↓ α∧␈↓circumscription, the function ␈↓↓city␈↓ must be taken as variable.



␈↓ α∧␈↓␈↓ αT6. A More general treatment of an ␈↓↓is-a␈↓ hierarchy
␈↓ α∧␈↓␈↓ f11


␈↓ α∧␈↓␈↓ αTThe␈α∞bird␈α∞example␈α∞works␈α∞fine␈α∞when␈α∞a␈α∞fixed␈α∞␈↓↓is-a␈↓␈α∞hierarchy␈α∞is␈α∞in␈α∞question.␈α∞ However,␈α
our

␈↓ α∧␈↓writing␈αthe␈αinheritance␈αcancellation␈αaxioms␈αdepended␈αon␈αknowing␈αexactly␈αfrom␈αwhat␈αhigher␈αlevel

␈↓ α∧␈↓the␈α∪properties␈α∩were␈α∪inherited.␈α∩ This␈α∪doesn't␈α∩correspond␈α∪to␈α∩my␈α∪intuition␈α∩of␈α∪how␈α∪we␈α∩humans

␈↓ α∧␈↓represent␈α∩inheritance.␈α∩ It␈α∩would␈α∪seem␈α∩rather␈α∩that␈α∩when␈α∩we␈α∪say␈α∩that␈α∩birds␈α∩can␈α∩fly,␈α∪we␈α∩don't

␈↓ α∧␈↓necessarily␈α∞have␈α∞in␈α∞mind␈α∞that␈α
an␈α∞inheritance␈α∞of␈α∞inability␈α∞to␈α
fly␈α∞from␈α∞things␈α∞in␈α∞general␈α∞is␈α
being

␈↓ α∧␈↓cancelled.␈α
 We␈α
can␈α
formulate␈α
inheritance␈α
of␈α
properties␈α
in␈α
a␈α
more␈α
general␈α
way␈α
provided␈α
we␈αreify

␈↓ α∧␈↓the properties.  Presumably there are many ways of doing this, but here's one that seems to work.

␈↓ α∧␈↓␈↓ αTThe␈α∂first␈α∂order␈α∂variables␈α∂of␈α∂our␈α∂theory␈α∂range␈α∂over␈α∂classes␈α∂of␈α∂objects␈α∂(denoted␈α∂by␈α∂␈↓↓c␈↓␈α∞with

␈↓ α∧␈↓numerical␈α
suffixes),␈α
properties␈α
(denoted␈α
by␈α
␈↓↓p)␈↓␈α
and␈α
objects␈α
(denoted␈α
by␈α
␈↓↓x).␈↓␈α
We␈α
need␈α∞not␈α
identify

␈↓ α∧␈↓classes␈α∩with␈α∩sets␈α∩(or␈α∩with␈α∩the␈α∩classes␈α∩of␈α∩GB␈α∩set␈α∩theory).␈α∩ In␈α∩particular,␈α∩we␈α∩need␈α∩not␈α⊃assume

␈↓ α∧␈↓extensionality.  We have several predicates:

␈↓ α∧␈↓␈↓ αT␈↓↓ordinarily(c,p)␈↓␈αmeans␈αthat␈αobjects␈αof␈αclass␈α␈↓↓c␈↓␈αordinarily␈αhave␈αproperty␈α␈↓↓p.␈↓␈α␈↓↓c1 ≤ c2␈↓␈αmeans␈αthat

␈↓ α∧␈↓class␈α␈↓↓c1␈↓␈α
ordinarily␈αinherits␈α
from␈αclass␈α
␈↓↓c2.␈↓␈αWe␈α
assume␈αthat␈α
this␈αrelation␈α
is␈αtransitive.␈α ␈↓↓in(x,c)␈↓␈α
means

␈↓ α∧␈↓that the object ␈↓↓x␈↓ is in class ␈↓↓c.␈↓ ␈↓↓ap(p,x)␈↓ means that property ␈↓↓p␈↓ applies to object ␈↓↓x.␈↓ Our axioms are

␈↓ α∧␈↓␈↓ αT22)␈↓ αt ␈↓↓∀c1 c2 c3. c1 ≤ c2 ∧ c2 ≤ c3 ⊃ c1 ≤ c3␈↓,

␈↓ α∧␈↓␈↓ αT23)␈↓ αt ␈↓↓∀c1 c2 p.ordinarily(c2,p) ∧ c1 ≤ c2 ∧ ¬ab aspect1(c1,c2,p) ⊃ ordinarily(c1,p)␈↓,

␈↓ α∧␈↓␈↓ αT24)␈↓ αt ␈↓↓∀c1 c2 c3 p.c1 ≤ c2 ∧ c2 ≤ c3 ∧ ordinarily(c2, not p) ⊃ ab aspect1(c1,c3,p)␈↓,

␈↓ α∧␈↓␈↓ αT25)␈↓ αt ␈↓↓∀x c p.in(x,c) ∧ ordinarily(c,p) ∧ ¬ab aspect3(x,c,p) ⊃ ap(p,x)␈↓,

␈↓ α∧␈↓␈↓ αT26)␈↓ αt ␈↓↓∀x c1 c2 p.in(x,c1) ∧ c1 ≤ c2 ∧ ordinarily(c1,not p) ⊃ ab aspect3(x,c2,p)␈↓.

␈↓ α∧␈↓␈↓ αT(22)␈α
is␈α
the␈αafore-mentioned␈α
transitivity␈α
of␈α≤.␈α
 (23)␈α
says␈αthat␈α
properties␈α
that␈α
ordinarily␈αhold

␈↓ α∧␈↓for␈αa␈αclass␈αare␈αinherited␈αunless␈αsomething␈αis␈αabnormal.␈α (24)␈αcancels␈αthe␈αinheritance␈αif␈αthere␈αis␈αan

␈↓ α∧␈↓intermediate␈αclass␈αfor␈αwhich␈αthe␈αproperty␈αordinarily␈αdoesn't␈αhold.␈α (25)␈αsays␈αthat␈αproperties␈αwhich

␈↓ α∧␈↓ordinarily␈αhold␈αactually␈αhold␈αfor␈αelements␈αof␈αthe␈αclass␈αunless␈αsomething␈αis␈αabnormal.␈α (26)␈αcancels

␈↓ α∧␈↓the␈α⊂effect␈α⊂of␈α⊂(25)␈α⊂when␈α⊂their␈α⊂is␈α⊂an␈α⊂intermediate␈α⊂class␈α⊂for␈α⊂which␈α⊂the␈α⊂negation␈α⊂of␈α⊃the␈α⊂property
␈↓ α∧␈↓␈↓ f12


␈↓ α∧␈↓ordinarily␈α⊂holds.␈α⊃ Notice␈α⊂that␈α⊃this␈α⊂reification␈α⊂of␈α⊃properties␈α⊂seems␈α⊃to␈α⊂require␈α⊃imitation␈α⊂boolean

␈↓ α∧␈↓operators.  Such operators are discussed in (McCarthy 1979).



␈↓ α∧␈↓␈↓ αT7. The blocks world

␈↓ α∧␈↓␈↓ αTThe␈α
following␈α
set␈α
of␈α"situation␈α
calculus"␈α
axioms␈α
solves␈α
the␈αframe␈α
problem␈α
for␈α
a␈αblocks␈α
world

␈↓ α∧␈↓in␈α∂which␈α∞blocks␈α∂can␈α∞be␈α∂moved␈α∞and␈α∂painted.␈α∞ Here␈α∂␈↓↓result(e,s)␈↓␈α∞denotes␈α∂the␈α∞situation␈α∂that␈α∞results

␈↓ α∧␈↓when␈α
event␈α␈↓↓e␈↓␈α
occurs␈αin␈α
situation␈α␈↓↓s.␈↓␈α
The␈αformalism␈α
is␈αapproximately␈α
that␈αof␈α
(McCarthy␈αand␈α
Hayes

␈↓ α∧␈↓1969).

␈↓ α∧␈↓␈↓ αT27)␈↓ αt ␈↓↓∀x e s.¬ab aspect1(x,e,s) ⊃ location(x,result(e,s)) = location(x,s)␈↓.

␈↓ α∧␈↓␈↓ αT28)␈↓ αt ␈↓↓∀x e s.¬ab aspect2(x,e,s) ⊃ color(x,result(e,s)) = color(x,s)␈↓.

␈↓ α∧␈↓␈↓ αTObjects change their locations and colors only for a reason.

␈↓ α∧␈↓␈↓ αT29)␈↓ αt ␈↓↓∀x l s.ab aspect1(x,move(x,l),s)␈↓

␈↓ α∧␈↓␈↓ αTand

␈↓ α∧␈↓␈↓ αT␈↓↓∀x l s.¬ab aspect3(x,l,s) ⊃ location(x,result(move(x,l),s)) = l␈↓.

␈↓ α∧␈↓␈↓ αT30)␈↓ αt ␈↓↓∀x c s.ab aspect2(x,paint(x,c),s)␈↓

␈↓ α∧␈↓␈↓ αTand

␈↓ α∧␈↓␈↓ αT␈↓↓∀x c s.¬ab aspect4(x,c,s) ⊃ color(x,result(paint(x,c),s)) = c␈↓.

␈↓ α∧␈↓␈↓ αTObjects change their locations when moved and their colors when painted.

␈↓ α∧␈↓␈↓ αT31)␈↓ αt ␈↓↓∀x l s.¬clear(top x,s) ∨ ¬clear(l,s) ∨ tooheavy x ∨ l = top x ⊃ ab aspect3(x,move(x,l),s)␈↓.

␈↓ α∧␈↓␈↓ αTThis␈αprevents␈α
the␈αrule␈α
(29)␈αfrom␈α
being␈αused␈αto␈α
infer␈αthat␈α
an␈αobject␈α
will␈αmove␈α
if␈αit␈αisn't␈α
clear

␈↓ α∧␈↓or␈α
to␈α
a␈α
destination␈α
that␈α
isn't␈α
clear␈α
or␈α
if␈αthe␈α
object␈α
is␈α
too␈α
heavy.␈α
 An␈α
object␈α
also␈α
cannot␈α
be␈αmoved␈α
to

␈↓ α∧␈↓its own top.

␈↓ α∧␈↓␈↓ αT32)␈↓ αt ␈↓↓∀l s.clear(l,s) ≡ ¬∃x.(¬trivial x ∧ location(x,s) = l)␈↓.

␈↓ α∧␈↓␈↓ αTA location is clear if all the objects there are trivial, e.g. a speck of dust.

␈↓ α∧␈↓␈↓ αT33)␈↓ αt ␈↓↓∀x.¬ab aspect7 x ⊃ ¬trivial x␈↓.
␈↓ α∧␈↓␈↓ f13


␈↓ α∧␈↓␈↓ αTTrivial objects are abnormal in ␈↓↓aspect7␈↓.



␈↓ α∧␈↓␈↓ αT8. An example of doing the circumscription.

␈↓ α∧␈↓␈↓ αTIn␈αorder␈αto␈αkeep␈αthe␈α
example␈αshort␈αwe␈αwill␈αtake␈α
into␈αaccount␈αonly␈αthe␈αfollowing␈α
facts␈αfrom

␈↓ α∧␈↓the previous section on flying.

␈↓ α∧␈↓␈↓ αT2) ␈↓↓∀x.¬ab aspect1 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓␈↓ αT3) ␈↓↓∀x.bird x ⊃ ab aspect1 x␈↓.

␈↓ α∧␈↓␈↓ αT4) ␈↓↓∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x␈↓.

␈↓ α∧␈↓␈↓ αT5) ␈↓↓∀x.ostrich x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓␈↓ αT7) ␈↓↓∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓␈↓ αTTheir␈α
conjunction␈α
is␈α
taken␈α
as␈α
␈↓↓A(ab,flies)␈↓.␈α This␈α
means␈α
that␈α
what␈α
entities␈α
satisfy␈α
␈↓↓ab␈↓␈αand␈α
what

␈↓ α∧␈↓entities␈α⊃satisfy␈α⊃␈↓↓flies␈↓␈α⊃are␈α⊃to␈α⊃be␈α⊃verified␈α⊃so␈α⊃as␈α⊃to␈α⊃minimize␈α⊃␈↓↓ab z.␈↓␈α⊃Which␈α⊃objects␈α⊃are␈α∩birds␈α⊃and

␈↓ α∧␈↓ostriches are parameters rather than variables, i.e.  what objects are birds is considered given.

␈↓ α∧␈↓␈↓ αTWe␈α
also␈αneed␈α
an␈αaxiom␈α
that␈α
asserts␈αthat␈α
the␈αaspects␈α
are␈α
different.␈α Here␈α
is␈αa␈α
straightforward

␈↓ α∧␈↓version that would be rather long were there more than three aspects.

␈↓ α∧␈↓␈↓ αT␈↓↓(∀x y.¬(aspect1 x = aspect2 y))

␈↓ α∧␈↓↓␈↓ αT∧ (∀x y.¬(aspect1 x = aspect3 y))

␈↓ α∧␈↓↓␈↓ αT∧ (∀x y.¬(aspect2 x = aspect3 y))

␈↓ α∧␈↓↓␈↓ αT∧ (∀x y.aspect1 x = aspect1 y ≡ x =y)

␈↓ α∧␈↓↓␈↓ αT∧ (∀x y.aspect2 x = aspect2 y ≡ x =y)

␈↓ α∧␈↓↓␈↓ αT∧ (∀x y.aspect3 x = aspect3 y ≡ x =y).␈↓

␈↓ α∧␈↓␈↓ αTThe circumscription formula ␈↓↓A'(ab,flies)␈↓ is then

␈↓ α∧␈↓␈↓ αT34)␈↓ αt ␈↓↓A(ab,flies) ∧ ∀ab' flies'.[A(ab',flies') ∧ [∀x. ab' x ⊃ ab x] ⊃ [∀x. ab x ≡ ab' x]]␈↓,

␈↓ α∧␈↓␈↓ αTwhich spelled out becomes
␈↓ α∧␈↓␈↓ f14


␈↓ α∧␈↓␈↓ αT35)␈↓ αt␈α␈↓↓[∀x.¬ab␈α
aspect1␈αx␈α
⊃␈α¬flies␈αx]␈α
∧␈α[∀x.bird␈α
x␈α⊃␈α
ab␈αaspect1␈αx]␈α
∧␈α[∀x.bird␈α
x␈α∧␈α
¬ab␈αaspect2␈αx␈α
⊃

␈↓ α∧␈↓↓flies␈α⊃x]␈α⊃∧␈α⊃[∀x.ostrich␈α⊃x␈α⊃⊃␈α⊃ab␈α⊃aspect2␈α⊃x]␈α∩∧␈α⊃[∀x.ostrich␈α⊃x␈α⊃∧␈α⊃¬ab␈α⊃aspect3␈α⊃x␈α⊃⊃␈α⊃¬flies␈α⊃x]␈α∩∧␈α⊃∀ab'

␈↓ α∧␈↓↓flies'.[[∀x.¬ab'␈αaspect1␈αx␈α⊃␈α¬flies'␈αx]␈α∧␈α[∀x.bird␈αx␈α⊃␈αab'␈αaspect1␈αx]␈α∧␈α[∀x.bird␈αx␈α∧␈α¬ab'␈αaspect2␈αx

␈↓ α∧␈↓↓⊃␈α
flies'␈α
x]␈α
∧␈α
[∀x.ostrich␈αx␈α
⊃␈α
ab'␈α
aspect2␈α
x]␈α∧␈α
[∀x.ostrich␈α
x␈α
∧␈α
¬ab'␈α
aspect3␈αx␈α
⊃␈α
¬flies'␈α
x]␈α
∧␈α[∀z.ab'␈α
z

␈↓ α∧␈↓↓⊃ ab z] ⊃ [∀z.ab z ≡ ab' z]]␈↓.

␈↓ α∧␈↓␈↓ αT␈↓↓A(ab,flies)␈↓␈α
is␈α
guaranteed␈α
to␈α
be␈α
true,␈α
because␈α
it␈α
is␈α
part␈α
of␈α
what␈α
is␈α
assumed␈α
in␈α
our␈αcommon

␈↓ α∧␈↓sense data base.  Therefore (35) reduces to

␈↓ α∧␈↓␈↓ αT36)␈↓ αt␈↓↓∀ab'␈αflies'.[[∀x.¬ab'␈αaspect1␈α
x␈α⊃␈α¬flies'␈α
x]␈α∧␈α[∀x.bird␈αx␈α
⊃␈αab'␈αaspect1␈α
x]␈α∧␈α[∀x.bird␈α
x␈α∧

␈↓ α∧␈↓↓¬ab'␈α∂aspect2␈α∞x␈α∂⊃␈α∞flies'␈α∂x]␈α∞∧␈α∂[∀x.ostrich␈α∞x␈α∂⊃␈α∞ab'␈α∂aspect2␈α∞x]␈α∂∧␈α∞[∀x.ostrich␈α∂x␈α∞∧␈α∂¬ab'␈α∞aspect3␈α∂x␈α∞⊃

␈↓ α∧␈↓↓¬flies' x] ∧ [∀z.ab' z ⊃ ab z] ⊃ [∀z.ab z ≡ ab' z]]␈↓.

␈↓ α∧␈↓␈↓ αTOur␈αobjective␈αis␈αnow␈αto␈αmake␈αsuitable␈αsubstitutions␈αfor␈α␈↓↓ab'␈↓␈αand␈α␈↓↓flies'␈↓␈αso␈αthat␈αall␈α
the␈αterms

␈↓ α∧␈↓preceding␈α∞the␈α∞⊃␈α∞(36)␈α∞will␈α∞be␈α∞true,␈α∂and␈α∞right␈α∞side␈α∞will␈α∞determine␈α∞␈↓↓ab.␈↓␈α∞The␈α∞axiom␈α∂␈↓↓A(ab,flies)␈↓␈α∞will

␈↓ α∧␈↓then␈α
determine␈α∞␈↓↓flies,␈↓␈α
i.e.␈α
we␈α∞will␈α
know␈α
what␈α∞the␈α
fliers␈α
are.␈α∞ ␈↓↓flies'␈↓␈α
is␈α
easy,␈α∞because␈α
we␈α∞need␈α
only

␈↓ α∧␈↓apply␈αwishful␈αthinking;␈αwe␈αwant␈αthe␈αfliers␈αto␈αbe␈αjust␈αthose␈αbirds␈αthat␈αaren't␈αostriches.␈α Therefore,

␈↓ α∧␈↓we put

␈↓ α∧␈↓␈↓ αT37)␈↓ αt ␈↓↓flies' x ≡ bird x ∧ ¬ostrich x␈↓.

␈↓ α∧␈↓␈↓ αT␈↓↓ab'␈↓ isn't really much more difficult, but there is a notational problem.  We define

␈↓ α∧␈↓␈↓ αT38)␈↓ αt ␈↓↓ab' z ≡ [∃x.bird x ∧ z = aspect1 x] ∨ [∃x.ostrich x ∧ z = aspect2 x]␈↓,

␈↓ α∧␈↓␈↓ αTwhich covers the cases we want to be abnormal.

␈↓ α∧␈↓␈↓ αTAppendix␈α∂A␈α∂contains␈α∂a␈α∞complete␈α∂proof␈α∂as␈α∂accepted␈α∞by␈α∂Jussi␈α∂Ketonen's␈α∂(1984)␈α∞interactive

␈↓ α∧␈↓theorem␈α⊂prover␈α⊂EKL.␈α⊂ EKL␈α⊂uses␈α∂the␈α⊂theory␈α⊂of␈α⊂types␈α⊂and␈α∂therefore␈α⊂has␈α⊂no␈α⊂problem␈α⊂with␈α∂the

␈↓ α∧␈↓second order logic required by circumscription.



␈↓ α∧␈↓␈↓ αT9. General considerations
␈↓ α∧␈↓␈↓ f15


␈↓ α∧␈↓␈↓ αTSuppose␈αwe␈α
have␈αa␈αdata␈α
base␈αof␈αfacts␈α
axiomatized␈αby␈αa␈α
formalism␈αinvolving␈α
the␈αpredicate

␈↓ α∧␈↓␈↓↓ab.␈↓␈α∩In␈α∩connection␈α∩with␈α∩a␈α∩particular␈α∩problem,␈α∩a␈α∩program␈α∩takes␈α∩a␈α∩subcollection␈α∩of␈α∩these␈α⊃facts

␈↓ α∧␈↓together␈α
with␈α
the␈αspecific␈α
facts␈α
of␈αthe␈α
problem␈α
and␈αthen␈α
circumscribes␈α
␈↓↓ab z.␈↓␈αWe␈α
get␈α
a␈αsecond␈α
order

␈↓ α∧␈↓formula,␈αand␈αin␈αgeneral,␈αas␈αthe␈αnatural␈αnumber␈αexample␈αof␈α(McCarthy␈α1980)␈αshows,␈αthis␈αformula

␈↓ α∧␈↓is␈α∀not␈α∀equivalent␈α∀to␈α∃any␈α∀first␈α∀order␈α∀formula.␈α∃ However,␈α∀many␈α∀common␈α∀sense␈α∃domains␈α∀are

␈↓ α∧␈↓axiomatizable␈αin␈α
such␈αa␈α
way␈αthat␈αthe␈α
circumscription␈αis␈α
equivalent␈αto␈αa␈α
first␈αorder␈α
formula.␈α For

␈↓ α∧␈↓example,␈α⊂Vladimir␈α⊂Lifschitz␈α⊂(1983)␈α⊂has␈α⊂shown␈α⊂that␈α∂this␈α⊂is␈α⊂true␈α⊂if␈α⊂the␈α⊂axioms␈α⊂are␈α⊂a␈α∂universal

␈↓ α∧␈↓formula␈α⊂and␈α⊂there␈α∂are␈α⊂no␈α⊂functions.␈α∂ This␈α⊂can␈α⊂presumably␈α∂be␈α⊂extended␈α⊂to␈α∂the␈α⊂case␈α⊂when␈α∂the

␈↓ α∧␈↓ranges␈αand␈α
domains␈αof␈α
the␈αfunctions␈αare␈α
disjoint,␈αso␈α
that␈αthere␈αis␈α
no␈αway␈α
of␈αgenerating␈αan␈α
infinity

␈↓ α∧␈↓of elements.

␈↓ α∧␈↓␈↓ αTWe␈α⊃can␈α⊃then␈α⊃regard␈α⊃the␈α⊃process␈α⊃of␈α⊃deciding␈α⊃what␈α⊃facts␈α⊃to␈α⊃take␈α⊃into␈α⊃account␈α⊃and␈α⊂then

␈↓ α∧␈↓circumscribing␈α
as␈α
a␈αprocess␈α
of␈α
compiling␈αfrom␈α
a␈α
slightly␈αhigher␈α
level␈α
non-monotonic␈αlanguage␈α
into

␈↓ α∧␈↓mathematical␈α∞logic,␈α∂especially␈α∞first␈α∂order␈α∞logic.␈α∂ We␈α∞can␈α∂also␈α∞regard␈α∂natural␈α∞language␈α∂as␈α∞higher

␈↓ α∧␈↓level␈α∃than␈α∃logic,␈α∃although,␈α∃as␈α∃I␈α∃shall␈α∃discuss␈α∃elsewhere,␈α∃natural␈α∃language␈α∃doesn't␈α∃have␈α∀an

␈↓ α∧␈↓independent␈α∪reasoning␈α∪process,␈α∪because␈α∪most␈α∪natural␈α∪language␈α∪inferences␈α∀involve␈α∪suppressed

␈↓ α∧␈↓premisses␈α∞which␈α∞are␈α∞not␈α∂represented␈α∞in␈α∞natural␈α∞language␈α∞in␈α∂the␈α∞minds␈α∞of␈α∞the␈α∞people␈α∂doing␈α∞the

␈↓ α∧␈↓reasoning.



␈↓ α∧␈↓␈↓ αT␈↓αAppendix A␈↓

␈↓ α∧␈↓␈↓ αTCircumscription in a Proof Checker

␈↓ α∧␈↓␈↓ αTEKL␈αis␈αan␈αinteractive␈αproof␈αchecker␈α
for␈αthe␈αtheory␈αof␈αtypes.␈α The␈αpresent␈α
argument␈αmakes

␈↓ α∧␈↓use␈αof␈α
its␈αability␈α
to␈αdo␈α
second␈αorder␈α
logic.␈α Each␈αstep␈α
begins␈αwith␈α
a␈αcommand␈α
given␈αby␈α
the␈αuser.

␈↓ α∧␈↓This␈αis␈αusually␈αfollowed␈αby␈αthe␈αsentence␈αresulting␈αfrom␈αthe␈αstep,␈αbut␈αthis␈αis␈αomitted␈αfor␈α
definitions

␈↓ α∧␈↓when the information is contained in the command.  We follow each step by a brief explanation.

␈↓ α∧␈↓ε␈↓ αT1. (DEFINE A
␈↓ α∧␈↓ε␈↓ αT     |∀AB FLIES.A(AB,FLIES)≡
␈↓ α∧␈↓␈↓ f16


␈↓ α∧␈↓ε␈↓ αT                (∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
␈↓ α∧␈↓ε␈↓ αT                (∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧
␈↓ α∧␈↓ε␈↓ αT                (∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
␈↓ α∧␈↓ε␈↓ αT                (∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))| NIL)
␈↓ α∧␈↓ε␈↓ αTThis defines the second order predicate ␈↓↓A(ab,flies)␈↓ε, where ␈↓↓ab␈↓ε and
␈↓ α∧␈↓ε␈↓ αT␈↓↓flies␈↓ε are predicate variables.  Included here are the specific facts
␈↓ α∧␈↓ε␈↓ αTabout flying being taken into account.

␈↓ α∧␈↓ε␈↓ αT;labels: SIMPINFO
␈↓ α∧␈↓ε␈↓ αT2. (AXIOM
␈↓ α∧␈↓ε␈↓ αT    |(∀X Y.¬ASPECT1(X)=ASPECT2(Y))∧(∀X Y.¬ASPECT1(X)=ASPECT3(Y))∧
␈↓ α∧␈↓ε␈↓ αT     (∀X Y.¬ASPECT2(X)=ASPECT3(Y))∧(∀X Y.ASPECT1(X)=ASPECT1(Y)≡X=Y)∧
␈↓ α∧␈↓ε␈↓ αT     (∀X Y.ASPECT2(X)=ASPECT2(Y)≡X=Y)∧(∀X Y.ASPECT3(X)=ASPECT3(Y)≡X=Y)|)
␈↓ α∧␈↓ε␈↓ αTThese facts about the distinctness of aspects are used in step 26 only.
␈↓ α∧␈↓ε␈↓ αTSince axiom 2 is labelled SIMPINFO, the EKL simplifier uses it
␈↓ α∧␈↓ε␈↓ αTwhen appropriate when it is asked to simplify a formula.

␈↓ α∧␈↓ε␈↓ αT3. (DEFINE A1
␈↓ α∧␈↓ε␈↓ αT     |∀AB FLIES.A1(AB,FLIES)≡
␈↓ α∧␈↓ε␈↓ αT                A(AB,FLIES)∧
␈↓ α∧␈↓ε␈↓ αT                (∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))|
␈↓ α∧␈↓ε␈↓ αT     NIL)
␈↓ α∧␈↓ε␈↓ αTThis is the circumscription formula itself.

␈↓ α∧␈↓ε␈↓ αT4. (ASSUME |A1(AB,FLIES)|)
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓ε␈↓ αTSince EKL cannot be asked (yet) to do a circumscription, we assume the
␈↓ α∧␈↓ε␈↓ αTresult.  Most subsequent statements list line 4 as a dependency.
␈↓ α∧␈↓ε␈↓ αTThis is appropriate since circumscription is a rule of conjecture rather
␈↓ α∧␈↓ε␈↓ αTthan a rule of inference.

␈↓ α∧␈↓ε␈↓ αT5. (DEFINE FLIES2 |∀X.FLIES2(X)≡BIRD(X)∧¬OSTRICH(X)| NIL)
␈↓ α∧␈↓ε␈↓ αTThis definition and the next say what we are going to substitute for
␈↓ α∧␈↓ε␈↓ αTthe bound predicate variables.

␈↓ α∧␈↓ε␈↓ αT6. (DEFINE AB2
␈↓ α∧␈↓ε␈↓ αT     |∀Z.AB2(Z)≡(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))|
␈↓ α∧␈↓ε␈↓ αTNIL)
␈↓ α∧␈↓ε␈↓ αTThe fact that this definition is necessarily somewhat awkward makes
␈↓ α∧␈↓ε␈↓ αTfor some difficulty throughout the proof.

␈↓ α∧␈↓ε␈↓ αT7. (RW 4 (OPEN A1))
␈↓ α∧␈↓ε␈↓ αTA(AB,FLIES)∧(∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓ε␈↓ αTThis step merely expands out the circumscription formula.

␈↓ α∧␈↓ε␈↓ αT8. (TRW |A(AB,FLIES)| (USE 7))
␈↓ α∧␈↓ε␈↓ αTA(AB,FLIES)
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓ε␈↓ αTWe separate the two conjuncts of 7 in this and the next step.

␈↓ α∧␈↓ε␈↓ αT9. (TRW |∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))|
␈↓ α∧␈↓ε␈↓ αT(USE 7))
␈↓ α∧␈↓ε␈↓ αT∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓␈↓ f17


␈↓ α∧␈↓ε␈↓ αT10. (RW 8 (OPEN A))
␈↓ α∧␈↓ε␈↓ αT(∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
␈↓ α∧␈↓ε␈↓ αT(∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧(∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
␈↓ α∧␈↓ε␈↓ αT(∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓ε␈↓ αTExpanding out the axiom using the definition ␈↓↓a␈↓ε in step 1.

␈↓ α∧␈↓ε␈↓ αT11. (ASSUME |AB2(Z)|)
␈↓ α∧␈↓ε␈↓ αTdeps: (11)
␈↓ α∧␈↓ε␈↓ αTOur goal is step 15, but we need to assume its premiss and then
␈↓ α∧␈↓ε␈↓ αTderive its conclusion.

␈↓ α∧␈↓ε␈↓ αT12. (RW 11 (OPEN AB2))
␈↓ α∧␈↓ε␈↓ αT(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))
␈↓ α∧␈↓ε␈↓ αTdeps: (11)
␈↓ α∧␈↓ε␈↓ αTWe use the definition of ␈↓↓ab2␈↓ε.

␈↓ α∧␈↓ε␈↓ αT13. (DERIVE |AB(Z)| (12 10) NIL)
␈↓ α∧␈↓ε␈↓ αTAB(Z)
␈↓ α∧␈↓ε␈↓ αTdeps: (4 11)
␈↓ α∧␈↓ε␈↓ αTHere EKL did a lot of work using its DERIVE command.  It took about
␈↓ α∧␈↓ε␈↓ αTten seconds of computer time on this step.

␈↓ α∧␈↓ε␈↓ αT14. (CI (11) 13 NIL)
␈↓ α∧␈↓ε␈↓ αTAB2(Z)⊃AB(Z)
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓ε␈↓ αTWe discharge the assumption 11.

␈↓ α∧␈↓ε␈↓ αT15. (DERIVE |∀Z.AB2(Z)⊃AB(Z)| (14) NIL)
␈↓ α∧␈↓ε␈↓ αT∀Z.AB2(Z)⊃AB(Z)
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓ε␈↓ αTUniversal generalization.

␈↓ α∧␈↓ε␈↓ αT16. (DERIVE |∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X)| (5 6) NIL)
␈↓ α∧␈↓ε␈↓ αT∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X)
␈↓ α∧␈↓ε␈↓ αTWe need to show that ␈↓↓ab2␈↓ε satisfies the axiom defining ␈↓↓ab.␈↓ε  This
␈↓ α∧␈↓ε␈↓ αTtakes till step 22, because we have to do the parts separately if
␈↓ α∧␈↓ε␈↓ αTwe want DERIVE to do the work for us.

␈↓ α∧␈↓ε␈↓ αT17. (DERIVE |∀X.BIRD(X)⊃AB2(ASPECT1(X))| (5 6) NIL)
␈↓ α∧␈↓ε␈↓ αT∀X.BIRD(X)⊃AB2(ASPECT1(X))

␈↓ α∧␈↓ε␈↓ αT18. (DERIVE |∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X)| (5 6) NIL)
␈↓ α∧␈↓ε␈↓ αT∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X)

␈↓ α∧␈↓ε␈↓ αT19. (DERIVE |∀X.OSTRICH(X)⊃AB2(ASPECT2(X))| (5 6) NIL)
␈↓ α∧␈↓ε␈↓ αT∀X.OSTRICH(X)⊃AB2(ASPECT2(X))

␈↓ α∧␈↓ε␈↓ αT20. (DERIVE |∀X.OSTRICH(X)⊃¬FLIES2(X)| (5 6) NIL)
␈↓ α∧␈↓ε␈↓ αT∀X.OSTRICH(X)⊃¬FLIES2(X)
␈↓ α∧␈↓ε␈↓ αTOur subgoal was step 21 but DERIVE ran out of push down list when
␈↓ α∧␈↓ε␈↓ αTwe tried to do it in one step.

␈↓ α∧␈↓ε␈↓ αT21. (DERIVE |∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X)| (20) NIL)
␈↓ α∧␈↓ε␈↓ αT∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X)
␈↓ α∧␈↓␈↓ f18


␈↓ α∧␈↓ε␈↓ αT22. (DERIVE
␈↓ α∧␈↓ε␈↓ αT      |(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
␈↓ α∧␈↓ε␈↓ αT(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
␈↓ α∧␈↓ε␈↓ αT       (∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))| (16 17 18 19 20 21)
␈↓ α∧␈↓ε␈↓ αTNIL)
␈↓ α∧␈↓ε␈↓ αT(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
␈↓ α∧␈↓ε␈↓ αT(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
␈↓ α∧␈↓ε␈↓ αT(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))
␈↓ α∧␈↓ε␈↓ αTHere we form a conjunction.

␈↓ α∧␈↓ε␈↓ αT23. (UE ((AB.|AB2|) (FLIES.|FLIES2|)) 1 NIL)
␈↓ α∧␈↓ε␈↓ αTA(AB2,FLIES2)≡
␈↓ α∧␈↓ε␈↓ αT(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
␈↓ α∧␈↓ε␈↓ αT(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
␈↓ α∧␈↓ε␈↓ αT(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))
␈↓ α∧␈↓ε␈↓ αTNow we subsitute ␈↓↓ab2␈↓ε and ␈↓↓flies2␈↓ε in the definition of ␈↓↓A␈↓ε and get
␈↓ α∧␈↓ε␈↓ αTa result we can compare with step 22.

␈↓ α∧␈↓ε␈↓ αT24. (RW 23 (USE 22))
␈↓ α∧␈↓ε␈↓ αTA(AB2,FLIES2)
␈↓ α∧␈↓ε␈↓ αTWe have shown that ␈↓↓ab2␈↓ε and ␈↓↓flies2␈↓ε satisfy ␈↓↓A.␈↓ε

␈↓ α∧␈↓ε␈↓ αT25. (DERIVE |∀Z.AB(Z)≡AB2(Z)| (9 15 24) NIL)
␈↓ α∧␈↓ε␈↓ αT∀Z.AB(Z)≡AB2(Z)
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓ε␈↓ αT9 was the circumscription formula, and 15 and 24 are its two premisses,
␈↓ α∧␈↓ε␈↓ αTso we can now derive its conclusion.  Now we know exactly what entities
␈↓ α∧␈↓ε␈↓ αTare abnormal.

␈↓ α∧␈↓ε␈↓ αT26. (RW 8 ((USE 1 MODE: EXACT) ((USE 25 MODE: EXACT) (OPEN AB2))))
␈↓ α∧␈↓ε␈↓ αT(∀X.¬(∃X1.BIRD(X1)∧X=X1)⊃¬FLIES(X))∧
␈↓ α∧␈↓ε␈↓ αT(∀X.BIRD(X)∧¬(∃X2.OSTRICH(X2)∧X=X2)⊃FLIES(X))∧(∀X.OSTRICH(X)⊃¬FLIES(X))
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓ε␈↓ αTWe rewrite the axiom now that we know what's abnormal.  This gives
␈↓ α∧␈↓ε␈↓ αTa somewhat awkward formula that nevertheless contains the desired
␈↓ α∧␈↓ε␈↓ αTconclusion.  The occurrences of equality are left over from the
␈↓ α∧␈↓ε␈↓ αTelimination of the aspects that used the axiom of step 2.  You should
␈↓ α∧␈↓ε␈↓ αTsee what step 26 looked like before we got that axiom properly
␈↓ α∧␈↓ε␈↓ αTformulated.

␈↓ α∧␈↓ε␈↓ αT27. (DERIVE |∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)| (26) NIL)
␈↓ α∧␈↓ε␈↓ αT∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)
␈↓ α∧␈↓ε␈↓ αTdeps: (4)
␈↓ α∧␈↓␈↓ αTDERIVE straightens out 26 to put the conclusion in the desired form.
␈↓ α∧␈↓␈↓ αTThe result is still dependent on the assumption of the correctness of
␈↓ α∧␈↓␈↓ αTthe circumscription made in step 4.

␈↓ α∧␈↓␈↓ αTClearly if circumscription is to become a practical technique,
␈↓ α∧␈↓␈↓ αTthe reasoning has to become much more automatic.



␈↓ α∧␈↓␈↓ αT10. References:
␈↓ α∧␈↓␈↓ f19


␈↓ α∧␈↓␈↓ αT␈↓αKetonen,␈α
Jussi␈α
and␈α
Joseph␈αS.␈α
Weening␈α
(1984)␈↓:␈α
␈↓↓EKL␈α-␈α
An␈α
Interactive␈α
Proof␈αChecker,␈α
User's

␈↓ α∧␈↓↓Reference Manual␈↓, Computer Science Department, Stanford University.

␈↓ α∧␈↓␈↓ αT␈↓αMcCarthy,␈αJohn␈αand␈αP.J.␈αHayes␈α(1969)␈↓:␈α"Some␈αPhilosophical␈αProblems␈αfrom␈αthe␈αStandpoint

␈↓ α∧␈↓of␈α
Artificial␈α
Intelligence",␈αin␈α
D.␈α
Michie␈α(ed),␈α
␈↓↓Machine␈α
Intelligence␈α4␈↓,␈α
American␈α
Elsevier,␈αNew␈α
York,

␈↓ α∧␈↓NY.

␈↓ α∧␈↓␈↓ αT␈↓αMcCarthy,␈αJohn␈α(1979)␈↓:␈α"First␈αOrder␈αTheories␈αof␈αIndividual␈αConcepts␈αand␈αPropositions",␈αin

␈↓ α∧␈↓Michie, Donald (ed.) ␈↓↓Machine Intelligence 9␈↓, (University of Edinburgh Press, Edinburgh).

␈↓ α∧␈↓␈↓ αT␈↓αMcCarthy,␈α↔John␈α↔(1980)␈↓:␈α↔"Circumscription␈α↔-␈α↔A␈α↔Form␈α↔of␈α_Non-Monotonic␈α↔Reasoning",

␈↓ α∧␈↓␈↓↓Artificial Intelligence␈↓, Volume 13, Numbers 1,2, April.

␈↓ α∧␈↓␈↓ αT␈↓αEtherington,␈α⊃David␈α⊃W.␈α⊃and␈α⊃Raymond␈α⊃Reiter␈α⊃(1983)␈↓:␈α⊃"On␈α⊃Inheritance␈α∩Hierarchies␈α⊃with

␈↓ α∧␈↓Exceptions",␈α∀in␈α∀␈↓↓Proceedings␈α∀of␈α∀the␈α∀National␈α∀Conference␈α∀on␈α∀Artificial␈α∀Intelligence,␈α∀AAAI-83␈↓,

␈↓ α∧␈↓William Kaufman, Inc.

␈↓ α∧␈↓␈↓ αTThis version of circum[f83,jmc] pubbed on April 9, 1984.